Nuprl Lemma : fpf-single_wf
0,22
postcript
pdf
A
:Type{j},
B
:(
A
Type{i}),
x
:
A
,
v
:
B
(
x
).
x
:
v
x
:
A
fp
B
(
x
)
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
P
Q
,
x
(
s
)
,
x
:
v
,
a
:
A
fp
B
(
a
)
Lemmas
l
member
wf
,
member
singleton
origin
A:Type{j}, B:(A
Type{i}), x:A, v:B(x). x : v 
x:A fp B(x) A:Type{j}, B:(AType{i}), x:A, v:B(x). x : v x:A fp B(x) T
Qx:A. B(x)
Q B(a)